(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 11))
(declare-fun v1 () (_ BitVec 6))
(declare-fun v2 () (_ BitVec 10))
(declare-fun v3 () (_ BitVec 1))
(declare-fun v4 () (_ BitVec 11))
(declare-fun a5 () (Array  (_ BitVec 2)  (_ BitVec 3)))
(declare-fun a6 () (Array  (_ BitVec 10)  (_ BitVec 16)))
(assert (let ((e7(_ bv2 2)))
(let ((e8(_ bv8 6)))
(let ((e9 (ite (bvsgt ((_ sign_extend 1) v2) v0) (_ bv1 1) (_ bv0 1))))
(let ((e10 (ite (bvule e7 ((_ sign_extend 1) v3)) (_ bv1 1) (_ bv0 1))))
(let ((e11 (ite (= v4 ((_ sign_extend 10) e10)) (_ bv1 1) (_ bv0 1))))
(let ((e12 (ite (bvuge ((_ zero_extend 5) v1) v4) (_ bv1 1) (_ bv0 1))))
(let ((e13 (ite (bvsgt v2 ((_ sign_extend 9) e12)) (_ bv1 1) (_ bv0 1))))
(let ((e14 (ite (bvslt e8 ((_ sign_extend 5) e11)) (_ bv1 1) (_ bv0 1))))
(let ((e15 (store a5 e7 ((_ sign_extend 2) e9))))
(let ((e16 (store a5 ((_ sign_extend 1) e11) ((_ zero_extend 2) e9))))
(let ((e17 (select e16 ((_ sign_extend 1) e10))))
(let ((e18 (select e16 ((_ extract 10 9) v4))))
(let ((e19 (select a5 ((_ zero_extend 1) e10))))
(let ((e20 (store e15 e7 ((_ zero_extend 2) e10))))
(let ((e21 (select a5 ((_ extract 1 0) v1))))
(let ((e22 (store e20 ((_ sign_extend 1) e13) ((_ zero_extend 2) e9))))
(let ((e23 (select e22 ((_ extract 3 2) v1))))
(let ((e24 (bvurem ((_ zero_extend 10) e14) v0)))
(let ((e25 (bvnor e11 e14)))
(let ((e26 (bvnot e23)))
(let ((e27 (ite (bvuge ((_ zero_extend 2) e13) e21) (_ bv1 1) (_ bv0 1))))
(let ((e28 (bvsdiv ((_ zero_extend 8) e26) v4)))
(let ((e29 (bvnor ((_ sign_extend 2) e9) e21)))
(let ((e30 (bvnand e10 e27)))
(let ((e31 (bvnot v1)))
(let ((e32 (bvurem ((_ sign_extend 3) e18) v1)))
(let ((e33 (ite (bvult e7 ((_ zero_extend 1) e27)) (_ bv1 1) (_ bv0 1))))
(let ((e34 (bvsub e17 e19)))
(let ((e35 (bvnot e12)))
(let ((e36 (bvudiv v3 e11)))
(let ((e37 (bvadd e8 ((_ sign_extend 3) e34))))
(let ((e38 ((_ zero_extend 2) e19)))
(let ((e39 (bvnot v2)))
(let ((e40 (bvugt e39 ((_ zero_extend 7) e17))))
(let ((e41 (bvsgt ((_ sign_extend 8) e21) e24)))
(let ((e42 (bvsge e37 ((_ sign_extend 5) e10))))
(let ((e43 (bvult v1 ((_ zero_extend 5) e13))))
(let ((e44 (bvsge ((_ zero_extend 5) e12) e8)))
(let ((e45 (distinct e23 e23)))
(let ((e46 (bvsle e21 ((_ zero_extend 1) e7))))
(let ((e47 (bvsge e11 e35)))
(let ((e48 (bvugt v2 ((_ sign_extend 4) e31))))
(let ((e49 (bvsge e39 ((_ zero_extend 4) v1))))
(let ((e50 (bvsgt e35 e13)))
(let ((e51 (bvsgt e17 ((_ zero_extend 2) e9))))
(let ((e52 (= e28 ((_ sign_extend 5) e31))))
(let ((e53 (distinct ((_ sign_extend 3) e18) v1)))
(let ((e54 (= ((_ zero_extend 10) e25) v0)))
(let ((e55 (bvsgt e12 e36)))
(let ((e56 (distinct ((_ zero_extend 10) e14) v4)))
(let ((e57 (= ((_ sign_extend 5) e8) e24)))
(let ((e58 (bvsgt e8 ((_ sign_extend 5) v3))))
(let ((e59 (bvuge e8 ((_ sign_extend 3) e23))))
(let ((e60 (bvult e30 e27)))
(let ((e61 (bvsge e19 e23)))
(let ((e62 (bvule e38 ((_ zero_extend 2) e19))))
(let ((e63 (distinct ((_ zero_extend 8) e19) v4)))
(let ((e64 (distinct v3 v3)))
(let ((e65 (bvslt e39 ((_ sign_extend 9) v3))))
(let ((e66 (bvule ((_ zero_extend 2) e30) e17)))
(let ((e67 (bvslt v0 ((_ sign_extend 1) e39))))
(let ((e68 (bvult ((_ zero_extend 3) e18) e32)))
(let ((e69 (bvult ((_ sign_extend 5) v3) e31)))
(let ((e70 (bvule e29 e34)))
(let ((e71 (= ((_ sign_extend 8) e26) e24)))
(let ((e72 (bvsgt e12 e10)))
(let ((e73 (bvult ((_ sign_extend 2) e10) e29)))
(let ((e74 (bvsge ((_ sign_extend 2) e14) e17)))
(let ((e75 (distinct ((_ zero_extend 2) e30) e17)))
(let ((e76 (bvuge ((_ zero_extend 9) e35) e39)))
(let ((e77 (bvsge e8 ((_ zero_extend 3) e21))))
(let ((e78 (bvuge e33 e33)))
(let ((e79 (= e51 e76)))
(let ((e80 (= e44 e63)))
(let ((e81 (and e57 e60)))
(let ((e82 (= e58 e68)))
(let ((e83 (not e54)))
(let ((e84 (and e65 e69)))
(let ((e85 (= e45 e66)))
(let ((e86 (=> e50 e49)))
(let ((e87 (and e48 e62)))
(let ((e88 (not e46)))
(let ((e89 (=> e74 e77)))
(let ((e90 (and e40 e52)))
(let ((e91 (not e88)))
(let ((e92 (ite e70 e79 e81)))
(let ((e93 (ite e61 e67 e87)))
(let ((e94 (not e92)))
(let ((e95 (= e75 e64)))
(let ((e96 (and e59 e53)))
(let ((e97 (= e55 e42)))
(let ((e98 (xor e73 e82)))
(let ((e99 (= e98 e47)))
(let ((e100 (xor e89 e94)))
(let ((e101 (and e78 e83)))
(let ((e102 (xor e95 e84)))
(let ((e103 (and e100 e90)))
(let ((e104 (=> e85 e93)))
(let ((e105 (ite e102 e41 e96)))
(let ((e106 (ite e43 e72 e71)))
(let ((e107 (and e104 e86)))
(let ((e108 (ite e105 e91 e80)))
(let ((e109 (or e106 e107)))
(let ((e110 (or e97 e99)))
(let ((e111 (or e109 e101)))
(let ((e112 (=> e56 e110)))
(let ((e113 (or e108 e103)))
(let ((e114 (=> e112 e111)))
(let ((e115 (=> e113 e113)))
(let ((e116 (or e114 e114)))
(let ((e117 (xor e116 e116)))
(let ((e118 (or e115 e117)))
(let ((e119 (and e118 (not (= v4 (_ bv0 11))))))
(let ((e120 (and e119 (not (= v4 (bvnot (_ bv0 11)))))))
(let ((e121 (and e120 (not (= v1 (_ bv0 6))))))
(let ((e122 (and e121 (not (= v0 (_ bv0 11))))))
(let ((e123 (and e122 (not (= e11 (_ bv0 1))))))
e123
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
